$\forall$$E$:Type, ${\it pred?}$:($E$$\rightarrow$($E$+Unit)).
\\[0ex]SWellFounded($\neg$first($y$) \& $x$ $=$ pred($y$) $\in$ $E$)
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:$E$. (${\it e'}$ $\in$ eventlist(${\it pred?}$;$e$)) $\Leftrightarrow$ (${\it e'}$ (($\lambda$$x$,$y$. $\neg$first($y$) \& $x$ $=$ pred($y$) $\in$ $E$)$^{\mbox{\scriptsize $\ast$}}$) $e$))